Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

Q is empty.


QTRS
  ↳ Non-Overlap Check

Q restricted rewrite system:
The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

Q is empty.

The TRS is non-overlapping. Hence, we can switch to innermost.

↳ QTRS
  ↳ Non-Overlap Check
QTRS
      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

The set Q consists of the following terms:

start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)


Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> BUSY7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b3, i3)
START1(i) -> BUSY7(F, closed, stop, false, false, false, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b2, i2)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b1, i1)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

The set Q consists of the following terms:

start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
QDP
          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> BUSY7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b3, i3)
START1(i) -> BUSY7(F, closed, stop, false, false, false, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b2, i2)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b1, i1)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

The set Q consists of the following terms:

start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 4 less nodes.

↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
QDP
              ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> BUSY7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

The set Q consists of the following terms:

start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be strictly oriented and are deleted.


IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> BUSY7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
The remaining pairs can at least by weakly be oriented.

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
Used ordering: Combined order from the following AFS and order.
BUSY7(x1, x2, x3, x4, x5, x6, x7)  =  BUSY3(x5, x6, x7)
S  =  S
closed  =  closed
stop  =  stop
true  =  true
false  =  false
IDLE7(x1, x2, x3, x4, x5, x6, x7)  =  IDLE3(x5, x6, x7)
down  =  down
newbuttons4(x1, x2, x3, x4)  =  newbuttons4(x1, x2, x3, x4)
or2(x1, x2)  =  or1(x2)
B  =  B
open  =  open
F  =  F
up  =  up
BF  =  BF
FS  =  FS
empty  =  empty

Lexicographic Path Order [19].
Precedence:
newbuttons4 > [BUSY3, IDLE3] > or1 > [S, true, false, open, F]
newbuttons4 > [BUSY3, IDLE3] > up > FS > closed > [S, true, false, open, F]


The following usable rules [14] were oriented:

or2(true, b) -> true
or2(false, b) -> b



↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ QDP
              ↳ QDPOrderProof
QDP
                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

The set Q consists of the following terms:

start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 3 less nodes.

↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ QDP
              ↳ QDPOrderProof
                ↳ QDP
                  ↳ DependencyGraphProof
QDP
                      ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

The set Q consists of the following terms:

start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be strictly oriented and are deleted.


BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
The remaining pairs can at least by weakly be oriented.

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
Used ordering: Combined order from the following AFS and order.
BUSY7(x1, x2, x3, x4, x5, x6, x7)  =  x6
S  =  S
closed  =  closed
stop  =  stop
true  =  true
false  =  false
IDLE7(x1, x2, x3, x4, x5, x6, x7)  =  x6
down  =  down
B  =  B
open  =  open
F  =  F
up  =  up
BF  =  BF
FS  =  FS
empty  =  empty

Lexicographic Path Order [19].
Precedence:
up > closed > true > false > [stop, down, F] > S > open
up > closed > true > false > [stop, down, F] > BF > B > open
up > closed > FS > [stop, down, F] > S > open
up > closed > FS > [stop, down, F] > BF > B > open
empty > open


The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ QDP
              ↳ QDPOrderProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ QDP
                      ↳ QDPOrderProof
QDP
                          ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

The set Q consists of the following terms:

start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be strictly oriented and are deleted.


BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
The remaining pairs can at least by weakly be oriented.

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
Used ordering: Combined order from the following AFS and order.
BUSY7(x1, x2, x3, x4, x5, x6, x7)  =  x4
S  =  S
closed  =  closed
stop  =  stop
true  =  true
false  =  false
IDLE7(x1, x2, x3, x4, x5, x6, x7)  =  x4
down  =  down
B  =  B
open  =  open
F  =  F
up  =  up
BF  =  BF
FS  =  FS
empty  =  empty

Lexicographic Path Order [19].
Precedence:
true > [S, up, FS] > [false, open] > [B, F, BF] > closed > stop > down
empty > down


The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ QDP
              ↳ QDPOrderProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ QDP
                      ↳ QDPOrderProof
                        ↳ QDP
                          ↳ QDPOrderProof
QDP
                              ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

The set Q consists of the following terms:

start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be strictly oriented and are deleted.


BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
The remaining pairs can at least by weakly be oriented.

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
Used ordering: Combined order from the following AFS and order.
BUSY7(x1, x2, x3, x4, x5, x6, x7)  =  BUSY5(x1, x2, x5, x6, x7)
S  =  S
closed  =  closed
stop  =  stop
true  =  true
false  =  false
IDLE7(x1, x2, x3, x4, x5, x6, x7)  =  IDLE5(x1, x2, x5, x6, x7)
down  =  down
B  =  B
open  =  open
F  =  F
up  =  up
BF  =  BF
FS  =  FS
empty  =  empty

Lexicographic Path Order [19].
Precedence:
true > [BUSY5, IDLE5] > false > [S, closed, stop, down, B, open, F, up, BF, FS]
empty > [BUSY5, IDLE5] > false > [S, closed, stop, down, B, open, F, up, BF, FS]


The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ QDP
              ↳ QDPOrderProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ QDP
                      ↳ QDPOrderProof
                        ↳ QDP
                          ↳ QDPOrderProof
                            ↳ QDP
                              ↳ QDPOrderProof
QDP
                                  ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

The set Q consists of the following terms:

start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be strictly oriented and are deleted.


BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
The remaining pairs can at least by weakly be oriented.

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
Used ordering: Combined order from the following AFS and order.
BUSY7(x1, x2, x3, x4, x5, x6, x7)  =  BUSY4(x2, x3, x4, x6)
S  =  S
closed  =  closed
stop  =  stop
true  =  true
false  =  false
IDLE7(x1, x2, x3, x4, x5, x6, x7)  =  IDLE4(x2, x3, x4, x6)
down  =  down
F  =  F
BF  =  BF
FS  =  FS
B  =  B
up  =  up
open  =  open
empty  =  empty

Lexicographic Path Order [19].
Precedence:
open > [BUSY4, IDLE4]


The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ QDP
              ↳ QDPOrderProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ QDP
                      ↳ QDPOrderProof
                        ↳ QDP
                          ↳ QDPOrderProof
                            ↳ QDP
                              ↳ QDPOrderProof
                                ↳ QDP
                                  ↳ QDPOrderProof
QDP

Q DP problem:
The TRS P consists of the following rules:

BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b

The set Q consists of the following terms:

start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)

We have to consider all minimal (P,Q,R)-chains.